the_es:ES, e', e:E.
(e  before(e'))  (l:E List. before(e') = (before(e) @ [e] @ l)  E List) 

latex

Definitions	ij, i<j, hd(l), l[i], firstn(n;as), S  T, Top, P  Q, t  ...$L, AB, A, False, ||as||, ij, (x  l), ES, P  Q, P & Q, P  Q, x:A. B(x), Prop, before(e), T, as @ bs, x:A. B(x), E, True, t  T
Lemmas	append wf, true wf, squash wf, es-before wf, l member decomp, event system wf, es-E wf, l member wf, length wf1, non neg length, firstn-before, length cons, length nil, length append, top wf, firstn length, firstn append, firstn wf, select wf, select append front, select append back, le wf